$\forall$$T$:Type, $P$:($T$$\rightarrow\mathbb{B}$), ${\it as}$:$T$ List, $d$:Top.
\\[0ex]($\exists$$a$:$T$. ($a$ $\in$ ${\it as}$) \& $P$($a$)) $\Rightarrow$ (first $a$ $\in$ ${\it as}$ s.t. $P$($a$) else $d$) $=$ hd(filter($\lambda$$a$.$P$($a$);${\it as}$)) $\in$ $T$